YES(O(1),O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Weak Trs:
  { #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We add following dependency tuples:

Strict DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , merge^#(@l1, @l2) -> c_2(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_3(merge#2^#(@l2, @x, @xs))
  , merge#1^#(nil(), @l2) -> c_4()
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_5(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys), #less^#(@x, @y))
  , merge#2^#(nil(), @x, @xs) -> c_6()
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_7(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_8(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> c_9(mergesort#1^#(@l))
  , mergesort#1^#(::(@x1, @xs)) -> c_10(mergesort#2^#(@xs, @x1))
  , mergesort#1^#(nil()) -> c_11()
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    c_12(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
         msplit^#(::(@x1, ::(@x2, @xs'))))
  , mergesort#2^#(nil(), @x1) -> c_13()
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    c_15(merge^#(mergesort(@l1), mergesort(@l2)),
         mergesort^#(@l1),
         mergesort^#(@l2))
  , msplit^#(@l) -> c_14(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_16(msplit#2^#(@xs, @x1))
  , msplit#1^#(nil()) -> c_17()
  , msplit#2^#(::(@x2, @xs'), @x1) ->
    c_18(msplit#3^#(msplit(@xs'), @x1, @x2), msplit^#(@xs'))
  , msplit#2^#(nil(), @x1) -> c_19()
  , msplit#3^#(tuple#2(@l1, @l2), @x1, @x2) -> c_20() }
Weak DPs:
  { #cklt^#(#EQ()) -> c_33()
  , #cklt^#(#GT()) -> c_34()
  , #cklt^#(#LT()) -> c_35()
  , #compare^#(#0(), #0()) -> c_21()
  , #compare^#(#0(), #neg(@y)) -> c_22()
  , #compare^#(#0(), #pos(@y)) -> c_23()
  , #compare^#(#0(), #s(@y)) -> c_24()
  , #compare^#(#neg(@x), #0()) -> c_25()
  , #compare^#(#neg(@x), #neg(@y)) -> c_26(#compare^#(@y, @x))
  , #compare^#(#neg(@x), #pos(@y)) -> c_27()
  , #compare^#(#pos(@x), #0()) -> c_28()
  , #compare^#(#pos(@x), #neg(@y)) -> c_29()
  , #compare^#(#pos(@x), #pos(@y)) -> c_30(#compare^#(@x, @y))
  , #compare^#(#s(@x), #0()) -> c_31()
  , #compare^#(#s(@x), #s(@y)) -> c_32(#compare^#(@x, @y)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , merge^#(@l1, @l2) -> c_2(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_3(merge#2^#(@l2, @x, @xs))
  , merge#1^#(nil(), @l2) -> c_4()
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_5(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys), #less^#(@x, @y))
  , merge#2^#(nil(), @x, @xs) -> c_6()
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_7(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_8(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> c_9(mergesort#1^#(@l))
  , mergesort#1^#(::(@x1, @xs)) -> c_10(mergesort#2^#(@xs, @x1))
  , mergesort#1^#(nil()) -> c_11()
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    c_12(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
         msplit^#(::(@x1, ::(@x2, @xs'))))
  , mergesort#2^#(nil(), @x1) -> c_13()
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    c_15(merge^#(mergesort(@l1), mergesort(@l2)),
         mergesort^#(@l1),
         mergesort^#(@l2))
  , msplit^#(@l) -> c_14(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_16(msplit#2^#(@xs, @x1))
  , msplit#1^#(nil()) -> c_17()
  , msplit#2^#(::(@x2, @xs'), @x1) ->
    c_18(msplit#3^#(msplit(@xs'), @x1, @x2), msplit^#(@xs'))
  , msplit#2^#(nil(), @x1) -> c_19()
  , msplit#3^#(tuple#2(@l1, @l2), @x1, @x2) -> c_20() }
Weak DPs:
  { #cklt^#(#EQ()) -> c_33()
  , #cklt^#(#GT()) -> c_34()
  , #cklt^#(#LT()) -> c_35()
  , #compare^#(#0(), #0()) -> c_21()
  , #compare^#(#0(), #neg(@y)) -> c_22()
  , #compare^#(#0(), #pos(@y)) -> c_23()
  , #compare^#(#0(), #s(@y)) -> c_24()
  , #compare^#(#neg(@x), #0()) -> c_25()
  , #compare^#(#neg(@x), #neg(@y)) -> c_26(#compare^#(@y, @x))
  , #compare^#(#neg(@x), #pos(@y)) -> c_27()
  , #compare^#(#pos(@x), #0()) -> c_28()
  , #compare^#(#pos(@x), #neg(@y)) -> c_29()
  , #compare^#(#pos(@x), #pos(@y)) -> c_30(#compare^#(@x, @y))
  , #compare^#(#s(@x), #0()) -> c_31()
  , #compare^#(#s(@x), #s(@y)) -> c_32(#compare^#(@x, @y)) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We estimate the number of application of {1,4,6,11,13,17,19,20} by
applications of Pre({1,4,6,11,13,17,19,20}) =
{2,3,5,9,10,15,16,18}. Here rules are labeled as follows:

  DPs:
    { 1: #less^#(@x, @y) ->
         c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
    , 2: merge^#(@l1, @l2) -> c_2(merge#1^#(@l1, @l2))
    , 3: merge#1^#(::(@x, @xs), @l2) -> c_3(merge#2^#(@l2, @x, @xs))
    , 4: merge#1^#(nil(), @l2) -> c_4()
    , 5: merge#2^#(::(@y, @ys), @x, @xs) ->
         c_5(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys), #less^#(@x, @y))
    , 6: merge#2^#(nil(), @x, @xs) -> c_6()
    , 7: merge#3^#(#false(), @x, @xs, @y, @ys) ->
         c_7(merge^#(::(@x, @xs), @ys))
    , 8: merge#3^#(#true(), @x, @xs, @y, @ys) ->
         c_8(merge^#(@xs, ::(@y, @ys)))
    , 9: mergesort^#(@l) -> c_9(mergesort#1^#(@l))
    , 10: mergesort#1^#(::(@x1, @xs)) -> c_10(mergesort#2^#(@xs, @x1))
    , 11: mergesort#1^#(nil()) -> c_11()
    , 12: mergesort#2^#(::(@x2, @xs'), @x1) ->
          c_12(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
               msplit^#(::(@x1, ::(@x2, @xs'))))
    , 13: mergesort#2^#(nil(), @x1) -> c_13()
    , 14: mergesort#3^#(tuple#2(@l1, @l2)) ->
          c_15(merge^#(mergesort(@l1), mergesort(@l2)),
               mergesort^#(@l1),
               mergesort^#(@l2))
    , 15: msplit^#(@l) -> c_14(msplit#1^#(@l))
    , 16: msplit#1^#(::(@x1, @xs)) -> c_16(msplit#2^#(@xs, @x1))
    , 17: msplit#1^#(nil()) -> c_17()
    , 18: msplit#2^#(::(@x2, @xs'), @x1) ->
          c_18(msplit#3^#(msplit(@xs'), @x1, @x2), msplit^#(@xs'))
    , 19: msplit#2^#(nil(), @x1) -> c_19()
    , 20: msplit#3^#(tuple#2(@l1, @l2), @x1, @x2) -> c_20()
    , 21: #cklt^#(#EQ()) -> c_33()
    , 22: #cklt^#(#GT()) -> c_34()
    , 23: #cklt^#(#LT()) -> c_35()
    , 24: #compare^#(#0(), #0()) -> c_21()
    , 25: #compare^#(#0(), #neg(@y)) -> c_22()
    , 26: #compare^#(#0(), #pos(@y)) -> c_23()
    , 27: #compare^#(#0(), #s(@y)) -> c_24()
    , 28: #compare^#(#neg(@x), #0()) -> c_25()
    , 29: #compare^#(#neg(@x), #neg(@y)) -> c_26(#compare^#(@y, @x))
    , 30: #compare^#(#neg(@x), #pos(@y)) -> c_27()
    , 31: #compare^#(#pos(@x), #0()) -> c_28()
    , 32: #compare^#(#pos(@x), #neg(@y)) -> c_29()
    , 33: #compare^#(#pos(@x), #pos(@y)) -> c_30(#compare^#(@x, @y))
    , 34: #compare^#(#s(@x), #0()) -> c_31()
    , 35: #compare^#(#s(@x), #s(@y)) -> c_32(#compare^#(@x, @y)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { merge^#(@l1, @l2) -> c_2(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_3(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_5(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys), #less^#(@x, @y))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_7(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_8(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> c_9(mergesort#1^#(@l))
  , mergesort#1^#(::(@x1, @xs)) -> c_10(mergesort#2^#(@xs, @x1))
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    c_12(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
         msplit^#(::(@x1, ::(@x2, @xs'))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    c_15(merge^#(mergesort(@l1), mergesort(@l2)),
         mergesort^#(@l1),
         mergesort^#(@l2))
  , msplit^#(@l) -> c_14(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_16(msplit#2^#(@xs, @x1))
  , msplit#2^#(::(@x2, @xs'), @x1) ->
    c_18(msplit#3^#(msplit(@xs'), @x1, @x2), msplit^#(@xs')) }
Weak DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , #cklt^#(#EQ()) -> c_33()
  , #cklt^#(#GT()) -> c_34()
  , #cklt^#(#LT()) -> c_35()
  , #compare^#(#0(), #0()) -> c_21()
  , #compare^#(#0(), #neg(@y)) -> c_22()
  , #compare^#(#0(), #pos(@y)) -> c_23()
  , #compare^#(#0(), #s(@y)) -> c_24()
  , #compare^#(#neg(@x), #0()) -> c_25()
  , #compare^#(#neg(@x), #neg(@y)) -> c_26(#compare^#(@y, @x))
  , #compare^#(#neg(@x), #pos(@y)) -> c_27()
  , #compare^#(#pos(@x), #0()) -> c_28()
  , #compare^#(#pos(@x), #neg(@y)) -> c_29()
  , #compare^#(#pos(@x), #pos(@y)) -> c_30(#compare^#(@x, @y))
  , #compare^#(#s(@x), #0()) -> c_31()
  , #compare^#(#s(@x), #s(@y)) -> c_32(#compare^#(@x, @y))
  , merge#1^#(nil(), @l2) -> c_4()
  , merge#2^#(nil(), @x, @xs) -> c_6()
  , mergesort#1^#(nil()) -> c_11()
  , mergesort#2^#(nil(), @x1) -> c_13()
  , msplit#1^#(nil()) -> c_17()
  , msplit#2^#(nil(), @x1) -> c_19()
  , msplit#3^#(tuple#2(@l1, @l2), @x1, @x2) -> c_20() }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ #less^#(@x, @y) ->
  c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, #cklt^#(#EQ()) -> c_33()
, #cklt^#(#GT()) -> c_34()
, #cklt^#(#LT()) -> c_35()
, #compare^#(#0(), #0()) -> c_21()
, #compare^#(#0(), #neg(@y)) -> c_22()
, #compare^#(#0(), #pos(@y)) -> c_23()
, #compare^#(#0(), #s(@y)) -> c_24()
, #compare^#(#neg(@x), #0()) -> c_25()
, #compare^#(#neg(@x), #neg(@y)) -> c_26(#compare^#(@y, @x))
, #compare^#(#neg(@x), #pos(@y)) -> c_27()
, #compare^#(#pos(@x), #0()) -> c_28()
, #compare^#(#pos(@x), #neg(@y)) -> c_29()
, #compare^#(#pos(@x), #pos(@y)) -> c_30(#compare^#(@x, @y))
, #compare^#(#s(@x), #0()) -> c_31()
, #compare^#(#s(@x), #s(@y)) -> c_32(#compare^#(@x, @y))
, merge#1^#(nil(), @l2) -> c_4()
, merge#2^#(nil(), @x, @xs) -> c_6()
, mergesort#1^#(nil()) -> c_11()
, mergesort#2^#(nil(), @x1) -> c_13()
, msplit#1^#(nil()) -> c_17()
, msplit#2^#(nil(), @x1) -> c_19()
, msplit#3^#(tuple#2(@l1, @l2), @x1, @x2) -> c_20() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { merge^#(@l1, @l2) -> c_2(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_3(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_5(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys), #less^#(@x, @y))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_7(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_8(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> c_9(mergesort#1^#(@l))
  , mergesort#1^#(::(@x1, @xs)) -> c_10(mergesort#2^#(@xs, @x1))
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    c_12(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
         msplit^#(::(@x1, ::(@x2, @xs'))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    c_15(merge^#(mergesort(@l1), mergesort(@l2)),
         mergesort^#(@l1),
         mergesort^#(@l2))
  , msplit^#(@l) -> c_14(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_16(msplit#2^#(@xs, @x1))
  , msplit#2^#(::(@x2, @xs'), @x1) ->
    c_18(msplit#3^#(msplit(@xs'), @x1, @x2), msplit^#(@xs')) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { merge#2^#(::(@y, @ys), @x, @xs) ->
    c_5(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys), #less^#(@x, @y))
  , msplit#2^#(::(@x2, @xs'), @x1) ->
    c_18(msplit#3^#(msplit(@xs'), @x1, @x2), msplit^#(@xs')) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> c_6(mergesort#1^#(@l))
  , mergesort#1^#(::(@x1, @xs)) -> c_7(mergesort#2^#(@xs, @x1))
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    c_8(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
        msplit^#(::(@x1, ::(@x2, @xs'))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    c_9(merge^#(mergesort(@l1), mergesort(@l2)),
        mergesort^#(@l1),
        mergesort^#(@l2))
  , msplit^#(@l) -> c_10(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_11(msplit#2^#(@xs, @x1))
  , msplit#2^#(::(@x2, @xs'), @x1) -> c_12(msplit^#(@xs')) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We decompose the input problem according to the dependency graph
into the upper component

  { mergesort^#(@l) -> c_6(mergesort#1^#(@l))
  , mergesort#1^#(::(@x1, @xs)) -> c_7(mergesort#2^#(@xs, @x1))
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    c_8(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
        msplit^#(::(@x1, ::(@x2, @xs'))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    c_9(merge^#(mergesort(@l1), mergesort(@l2)),
        mergesort^#(@l1),
        mergesort^#(@l2)) }

and lower component

  { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , msplit^#(@l) -> c_10(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_11(msplit#2^#(@xs, @x1))
  , msplit#2^#(::(@x2, @xs'), @x1) -> c_12(msplit^#(@xs')) }

Further, following extension rules are added to the lower
component.

{ mergesort^#(@l) -> mergesort#1^#(@l)
, mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
, mergesort#2^#(::(@x2, @xs'), @x1) ->
  mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
, mergesort#2^#(::(@x2, @xs'), @x1) ->
  msplit^#(::(@x1, ::(@x2, @xs')))
, mergesort#3^#(tuple#2(@l1, @l2)) ->
  merge^#(mergesort(@l1), mergesort(@l2))
, mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
, mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }

TcT solves the upper component with certificate YES(O(1),O(n^1)).

Sub-proof:
----------
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs:
    { mergesort^#(@l) -> c_6(mergesort#1^#(@l))
    , mergesort#1^#(::(@x1, @xs)) -> c_7(mergesort#2^#(@xs, @x1))
    , mergesort#2^#(::(@x2, @xs'), @x1) ->
      c_8(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
          msplit^#(::(@x1, ::(@x2, @xs'))))
    , mergesort#3^#(tuple#2(@l1, @l2)) ->
      c_9(merge^#(mergesort(@l1), mergesort(@l2)),
          mergesort^#(@l1),
          mergesort^#(@l2)) }
  Weak Trs:
    { #less(@x, @y) -> #cklt(#compare(@x, @y))
    , #compare(#0(), #0()) -> #EQ()
    , #compare(#0(), #neg(@y)) -> #GT()
    , #compare(#0(), #pos(@y)) -> #LT()
    , #compare(#0(), #s(@y)) -> #LT()
    , #compare(#neg(@x), #0()) -> #LT()
    , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
    , #compare(#neg(@x), #pos(@y)) -> #LT()
    , #compare(#pos(@x), #0()) -> #GT()
    , #compare(#pos(@x), #neg(@y)) -> #GT()
    , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
    , #compare(#s(@x), #0()) -> #GT()
    , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
    , #cklt(#EQ()) -> #false()
    , #cklt(#GT()) -> #false()
    , #cklt(#LT()) -> #true()
    , merge(@l1, @l2) -> merge#1(@l1, @l2)
    , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
    , merge#1(nil(), @l2) -> @l2
    , merge#2(::(@y, @ys), @x, @xs) ->
      merge#3(#less(@x, @y), @x, @xs, @y, @ys)
    , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
    , merge#3(#false(), @x, @xs, @y, @ys) ->
      ::(@y, merge(::(@x, @xs), @ys))
    , merge#3(#true(), @x, @xs, @y, @ys) ->
      ::(@x, merge(@xs, ::(@y, @ys)))
    , mergesort(@l) -> mergesort#1(@l)
    , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
    , mergesort#1(nil()) -> nil()
    , mergesort#2(::(@x2, @xs'), @x1) ->
      mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
    , mergesort#2(nil(), @x1) -> ::(@x1, nil())
    , msplit(@l) -> msplit#1(@l)
    , mergesort#3(tuple#2(@l1, @l2)) ->
      merge(mergesort(@l1), mergesort(@l2))
    , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
    , msplit#1(nil()) -> tuple#2(nil(), nil())
    , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
    , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
    , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
      tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(n^1))
  
  Due to missing edges in the dependency-graph, the right-hand sides
  of following rules could be simplified:
  
    { mergesort#2^#(::(@x2, @xs'), @x1) ->
      c_8(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))),
          msplit^#(::(@x1, ::(@x2, @xs'))))
    , mergesort#3^#(tuple#2(@l1, @l2)) ->
      c_9(merge^#(mergesort(@l1), mergesort(@l2)),
          mergesort^#(@l1),
          mergesort^#(@l2)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs:
    { mergesort^#(@l) -> c_1(mergesort#1^#(@l))
    , mergesort#1^#(::(@x1, @xs)) -> c_2(mergesort#2^#(@xs, @x1))
    , mergesort#2^#(::(@x2, @xs'), @x1) ->
      c_3(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))))
    , mergesort#3^#(tuple#2(@l1, @l2)) ->
      c_4(mergesort^#(@l1), mergesort^#(@l2)) }
  Weak Trs:
    { #less(@x, @y) -> #cklt(#compare(@x, @y))
    , #compare(#0(), #0()) -> #EQ()
    , #compare(#0(), #neg(@y)) -> #GT()
    , #compare(#0(), #pos(@y)) -> #LT()
    , #compare(#0(), #s(@y)) -> #LT()
    , #compare(#neg(@x), #0()) -> #LT()
    , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
    , #compare(#neg(@x), #pos(@y)) -> #LT()
    , #compare(#pos(@x), #0()) -> #GT()
    , #compare(#pos(@x), #neg(@y)) -> #GT()
    , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
    , #compare(#s(@x), #0()) -> #GT()
    , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
    , #cklt(#EQ()) -> #false()
    , #cklt(#GT()) -> #false()
    , #cklt(#LT()) -> #true()
    , merge(@l1, @l2) -> merge#1(@l1, @l2)
    , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
    , merge#1(nil(), @l2) -> @l2
    , merge#2(::(@y, @ys), @x, @xs) ->
      merge#3(#less(@x, @y), @x, @xs, @y, @ys)
    , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
    , merge#3(#false(), @x, @xs, @y, @ys) ->
      ::(@y, merge(::(@x, @xs), @ys))
    , merge#3(#true(), @x, @xs, @y, @ys) ->
      ::(@x, merge(@xs, ::(@y, @ys)))
    , mergesort(@l) -> mergesort#1(@l)
    , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
    , mergesort#1(nil()) -> nil()
    , mergesort#2(::(@x2, @xs'), @x1) ->
      mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
    , mergesort#2(nil(), @x1) -> ::(@x1, nil())
    , msplit(@l) -> msplit#1(@l)
    , mergesort#3(tuple#2(@l1, @l2)) ->
      merge(mergesort(@l1), mergesort(@l2))
    , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
    , msplit#1(nil()) -> tuple#2(nil(), nil())
    , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
    , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
    , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
      tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(n^1))
  
  We replace rewrite rules by usable rules:
  
    Weak Usable Rules:
      { msplit(@l) -> msplit#1(@l)
      , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
      , msplit#1(nil()) -> tuple#2(nil(), nil())
      , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
      , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
      , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
        tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs:
    { mergesort^#(@l) -> c_1(mergesort#1^#(@l))
    , mergesort#1^#(::(@x1, @xs)) -> c_2(mergesort#2^#(@xs, @x1))
    , mergesort#2^#(::(@x2, @xs'), @x1) ->
      c_3(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))))
    , mergesort#3^#(tuple#2(@l1, @l2)) ->
      c_4(mergesort^#(@l1), mergesort^#(@l2)) }
  Weak Trs:
    { msplit(@l) -> msplit#1(@l)
    , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
    , msplit#1(nil()) -> tuple#2(nil(), nil())
    , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
    , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
    , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
      tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(n^1))
  
  We use the processor 'matrix interpretation of dimension 3' to
  orient following rules strictly.
  
  DPs:
    { 4: mergesort#3^#(tuple#2(@l1, @l2)) ->
         c_4(mergesort^#(@l1), mergesort^#(@l2)) }
  
  Sub-proof:
  ----------
    The following argument positions are usable:
      Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
      Uargs(c_4) = {1, 2}
    
    TcT has computed following constructor-based matrix interpretation
    satisfying not(EDA) and not(IDA(1)).
    
                                        [0]
                      [#less](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
                   [#compare](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
                          [#cklt](x1) = [0]
                                        [0]
                                           
                                        [0]
                      [merge](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
                    [merge#1](x1, x2) = [0]
                                        [0]
                                           
                                        [0 0 0]      [0 0 1]      [0]
                         [::](x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [1]
                                        [0 1 0]      [0 0 1]      [1]
                                                                     
                                        [0]
                [merge#2](x1, x2, x3) = [0]
                                        [0]
                                           
                                        [0]
                                [nil] = [1]
                                        [0]
                                           
                                        [0]
        [merge#3](x1, x2, x3, x4, x5) = [0]
                                        [0]
                                           
                                        [0]
                             [#false] = [0]
                                        [0]
                                           
                                        [0]
                              [#true] = [0]
                                        [0]
                                           
                                        [0]
                      [mergesort](x1) = [0]
                                        [0]
                                           
                                        [0]
                    [mergesort#1](x1) = [0]
                                        [0]
                                           
                                        [0]
                [mergesort#2](x1, x2) = [0]
                                        [0]
                                           
                                        [0 0 1]      [0]
                         [msplit](x1) = [0 0 0] x1 + [1]
                                        [0 1 0]      [0]
                                                        
                                        [0]
                    [mergesort#3](x1) = [0]
                                        [0]
                                           
                                        [0 0 1]      [0 0 1]      [0]
                    [tuple#2](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [1]
                                        [1 0 0]      [1 0 0]      [1]
                                                                     
                                        [0 0 1]      [0]
                       [msplit#1](x1) = [0 0 0] x1 + [1]
                                        [0 1 0]      [0]
                                                        
                                        [0 0 1]      [0 1 0]      [1]
                   [msplit#2](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [1]
                                        [1 0 0]      [0 0 0]      [1]
                                                                     
                                        [1 1 0]      [0 1 0]      [0 1
                                                                   0]      [1]
               [msplit#3](x1, x2, x3) = [0 1 0] x1 + [0 0 0] x2 + [0 0
                                                                   0] x3 + [0]
                                        [1 1 0]      [0 0 0]      [0 0
                                                                   0]      [0]
                                                                              
                                        [0]
                                [#EQ] = [0]
                                        [0]
                                           
                                        [0]
                                [#GT] = [0]
                                        [0]
                                           
                                        [0]
                                [#LT] = [0]
                                        [0]
                                           
                                        [0]
                                 [#0] = [0]
                                        [0]
                                           
                                        [0 0 1]      [0]
                           [#neg](x1) = [0 1 0] x1 + [0]
                                        [1 0 0]      [0]
                                                        
                                        [0 0 1]      [0]
                           [#pos](x1) = [0 0 1] x1 + [0]
                                        [1 0 0]      [0]
                                                        
                                        [0 0 1]      [0]
                             [#s](x1) = [0 0 0] x1 + [0]
                                        [0 1 0]      [0]
                                                        
                                        [0]
                    [#less^#](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
                        [#cklt^#](x1) = [0]
                                        [0]
                                           
                                        [0]
                 [#compare^#](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
                    [merge^#](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
                  [merge#1^#](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
              [merge#2^#](x1, x2, x3) = [0]
                                        [0]
                                           
                                        [0]
      [merge#3^#](x1, x2, x3, x4, x5) = [0]
                                        [0]
                                           
                                        [1 0 0]      [0]
                    [mergesort^#](x1) = [0 0 0] x1 + [1]
                                        [0 0 0]      [1]
                                                        
                                        [1 0 0]      [0]
                  [mergesort#1^#](x1) = [0 0 0] x1 + [0]
                                        [0 0 0]      [0]
                                                        
                                        [0 0 1]      [0]
              [mergesort#2^#](x1, x2) = [0 0 0] x1 + [0]
                                        [0 0 0]      [1]
                                                        
                                        [0 0 1]      [0]
                  [mergesort#3^#](x1) = [0 1 0] x1 + [0]
                                        [0 0 0]      [0]
                                                        
                                        [0]
                       [msplit^#](x1) = [0]
                                        [0]
                                           
                                        [0]
                     [msplit#1^#](x1) = [0]
                                        [0]
                                           
                                        [0]
                 [msplit#2^#](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
             [msplit#3^#](x1, x2, x3) = [0]
                                        [0]
                                           
                                        [0]
                            [c_6](x1) = [0]
                                        [0]
                                           
                                        [0]
                            [c_7](x1) = [0]
                                        [0]
                                           
                                        [0]
                        [c_8](x1, x2) = [0]
                                        [0]
                                           
                                        [0]
                    [c_9](x1, x2, x3) = [0]
                                        [0]
                                           
                                        [0]
                                  [c] = [0]
                                        [0]
                                           
                                        [1 1 1]      [0]
                            [c_1](x1) = [0 0 0] x1 + [0]
                                        [0 0 0]      [0]
                                                        
                                        [1 0 0]      [0]
                            [c_2](x1) = [0 0 0] x1 + [0]
                                        [0 0 0]      [0]
                                                        
                                        [1 0 1]      [0]
                            [c_3](x1) = [0 0 0] x1 + [0]
                                        [0 0 0]      [0]
                                                        
                                        [1 0 0]      [1 0 0]      [0]
                        [c_4](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                                        [0 0 0]      [0 0 0]      [0]
    
    This order satisfies following ordering constraints
    
                                 [msplit(@l)] =  [0 0 1]      [0]                                           
                                                 [0 0 0] @l + [1]                                           
                                                 [0 1 0]      [0]                                           
                                              >= [0 0 1]      [0]                                           
                                                 [0 0 0] @l + [1]                                           
                                                 [0 1 0]      [0]                                           
                                              =  [msplit#1(@l)]                                             
                                                                                                            
                     [msplit#1(::(@x1, @xs))] =  [0 1 0]       [0 0 1]       [1]                            
                                                 [0 0 0] @x1 + [0 0 0] @xs + [1]                            
                                                 [0 0 0]       [1 0 0]       [1]                            
                                              >= [0 1 0]       [0 0 1]       [1]                            
                                                 [0 0 0] @x1 + [0 0 0] @xs + [1]                            
                                                 [0 0 0]       [1 0 0]       [1]                            
                                              =  [msplit#2(@xs, @x1)]                                       
                                                                                                            
                            [msplit#1(nil())] =  [0]                                                        
                                                 [1]                                                        
                                                 [1]                                                        
                                              >= [0]                                                        
                                                 [1]                                                        
                                                 [1]                                                        
                                              =  [tuple#2(nil(), nil())]                                    
                                                                                                            
               [msplit#2(::(@x2, @xs'), @x1)] =  [0 1 0]       [0 1 0]       [0 0 1]        [2]             
                                                 [0 0 0] @x1 + [0 0 0] @x2 + [0 0 0] @xs' + [1]             
                                                 [0 0 0]       [0 0 0]       [0 0 1]        [1]             
                                              >= [0 1 0]       [0 1 0]       [0 0 1]        [2]             
                                                 [0 0 0] @x1 + [0 0 0] @x2 + [0 0 0] @xs' + [1]             
                                                 [0 0 0]       [0 0 0]       [0 0 1]        [1]             
                                              =  [msplit#3(msplit(@xs'), @x1, @x2)]                         
                                                                                                            
                       [msplit#2(nil(), @x1)] =  [0 1 0]       [1]                                          
                                                 [0 0 0] @x1 + [1]                                          
                                                 [0 0 0]       [1]                                          
                                              >= [0 1 0]       [1]                                          
                                                 [0 0 0] @x1 + [1]                                          
                                                 [0 0 0]       [1]                                          
                                              =  [tuple#2(::(@x1, nil()), nil())]                           
                                                                                                            
      [msplit#3(tuple#2(@l1, @l2), @x1, @x2)] =  [0 0 1]       [0 0 1]       [0 1 0]       [0 1 0]       [2]
                                                 [0 0 0] @l1 + [0 0 0] @l2 + [0 0 0] @x1 + [0 0 0] @x2 + [1]
                                                 [0 0 1]       [0 0 1]       [0 0 0]       [0 0 0]       [1]
                                              >= [0 0 1]       [0 0 1]       [0 1 0]       [0 1 0]       [2]
                                                 [0 0 0] @l1 + [0 0 0] @l2 + [0 0 0] @x1 + [0 0 0] @x2 + [1]
                                                 [0 0 1]       [0 0 1]       [0 0 0]       [0 0 0]       [1]
                                              =  [tuple#2(::(@x1, @l1), ::(@x2, @l2))]                      
                                                                                                            
                            [mergesort^#(@l)] =  [1 0 0]      [0]                                           
                                                 [0 0 0] @l + [1]                                           
                                                 [0 0 0]      [1]                                           
                                              >= [1 0 0]      [0]                                           
                                                 [0 0 0] @l + [0]                                           
                                                 [0 0 0]      [0]                                           
                                              =  [c_1(mergesort#1^#(@l))]                                   
                                                                                                            
                [mergesort#1^#(::(@x1, @xs))] =  [0 0 1]       [0]                                          
                                                 [0 0 0] @xs + [0]                                          
                                                 [0 0 0]       [0]                                          
                                              >= [0 0 1]       [0]                                          
                                                 [0 0 0] @xs + [0]                                          
                                                 [0 0 0]       [0]                                          
                                              =  [c_2(mergesort#2^#(@xs, @x1))]                             
                                                                                                            
          [mergesort#2^#(::(@x2, @xs'), @x1)] =  [0 1 0]       [0 0 1]        [1]                           
                                                 [0 0 0] @x2 + [0 0 0] @xs' + [0]                           
                                                 [0 0 0]       [0 0 0]        [1]                           
                                              >= [0 0 1]        [1]                                         
                                                 [0 0 0] @xs' + [0]                                         
                                                 [0 0 0]        [0]                                         
                                              =  [c_3(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))))]       
                                                                                                            
           [mergesort#3^#(tuple#2(@l1, @l2))] =  [1 0 0]       [1 0 0]       [1]                            
                                                 [0 0 0] @l1 + [0 0 0] @l2 + [1]                            
                                                 [0 0 0]       [0 0 0]       [0]                            
                                              >  [1 0 0]       [1 0 0]       [0]                            
                                                 [0 0 0] @l1 + [0 0 0] @l2 + [0]                            
                                                 [0 0 0]       [0 0 0]       [0]                            
                                              =  [c_4(mergesort^#(@l1), mergesort^#(@l2))]                  
                                                                                                            
  
  Consider the set of all dependency pairs
  
  DPs:
    { 1: mergesort^#(@l) -> c_1(mergesort#1^#(@l))
    , 2: mergesort#1^#(::(@x1, @xs)) -> c_2(mergesort#2^#(@xs, @x1))
    , 3: mergesort#2^#(::(@x2, @xs'), @x1) ->
         c_3(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))))
    , 4: mergesort#3^#(tuple#2(@l1, @l2)) ->
         c_4(mergesort^#(@l1), mergesort^#(@l2)) }
  
  Processor 'matrix interpretation of dimension 3' induces the
  complexity certificate YES(?,O(n^1)) on application of dependency
  pairs {4}. These cover all (indirect) predecessors of dependency
  pairs {1,2,3,4}, their number of application is equally bounded.
  The dependency pairs are shifted into the corresponding weak
  component(s).
  
  We apply the transformation 'removetails' on the sub-problem:
  
  Weak DPs:
    { mergesort^#(@l) -> c_1(mergesort#1^#(@l))
    , mergesort#1^#(::(@x1, @xs)) -> c_2(mergesort#2^#(@xs, @x1))
    , mergesort#2^#(::(@x2, @xs'), @x1) ->
      c_3(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))))
    , mergesort#3^#(tuple#2(@l1, @l2)) ->
      c_4(mergesort^#(@l1), mergesort^#(@l2)) }
  Weak Trs:
    { msplit(@l) -> msplit#1(@l)
    , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
    , msplit#1(nil()) -> tuple#2(nil(), nil())
    , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
    , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
    , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
      tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
  StartTerms: basic terms
  Strategy: innermost
  
  The following weak DPs constitute a sub-graph of the DG that is
  closed under successors. The DPs are removed.
  
  { mergesort^#(@l) -> c_1(mergesort#1^#(@l))
  , mergesort#1^#(::(@x1, @xs)) -> c_2(mergesort#2^#(@xs, @x1))
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    c_3(mergesort#3^#(msplit(::(@x1, ::(@x2, @xs')))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    c_4(mergesort^#(@l1), mergesort^#(@l2)) }
  
  
  We apply the transformation 'usablerules' on the sub-problem:
  
  Weak Trs:
    { msplit(@l) -> msplit#1(@l)
    , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
    , msplit#1(nil()) -> tuple#2(nil(), nil())
    , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
    , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
    , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
      tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
  StartTerms: basic terms
  Strategy: innermost
  
  No rule is usable, rules are removed from the input problem.
  
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Rules: Empty
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(1))
  
  Empty rules are trivially bounded

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , msplit^#(@l) -> c_10(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_11(msplit#2^#(@xs, @x1))
  , msplit#2^#(::(@x2, @xs'), @x1) -> c_12(msplit^#(@xs')) }
Weak DPs:
  { mergesort^#(@l) -> mergesort#1^#(@l)
  , mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    msplit^#(::(@x1, ::(@x2, @xs')))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    merge^#(mergesort(@l1), mergesort(@l2))
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 5: merge#3^#(#true(), @x, @xs, @y, @ys) ->
       c_5(merge^#(@xs, ::(@y, @ys)))
  , 12: mergesort#2^#(::(@x2, @xs'), @x1) ->
        msplit^#(::(@x1, ::(@x2, @xs'))) }
Trs: { mergesort#2(nil(), @x1) -> ::(@x1, nil()) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
    Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_10) = {1},
    Uargs(c_11) = {1}, Uargs(c_12) = {1}
  
  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).
  
                    [#less](x1, x2) = [0]
                                         
                 [#compare](x1, x2) = [0]
                                         
                        [#cklt](x1) = [0]
                                         
                    [merge](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                  [merge#1](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                       [::](x1, x2) = [1] x2 + [1]
                                                  
              [merge#2](x1, x2, x3) = [1] x1 + [1] x3 + [1]
                                                           
                              [nil] = [0]
                                         
      [merge#3](x1, x2, x3, x4, x5) = [1] x3 + [1] x5 + [2]
                                                           
                           [#false] = [0]
                                         
                            [#true] = [0]
                                         
                    [mergesort](x1) = [2] x1 + [0]
                                                  
                  [mergesort#1](x1) = [2] x1 + [0]
                                                  
              [mergesort#2](x1, x2) = [2] x1 + [2]
                                                  
                       [msplit](x1) = [1] x1 + [0]
                                                  
                  [mergesort#3](x1) = [2] x1 + [0]
                                                  
                  [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                     [msplit#1](x1) = [1] x1 + [0]
                                                  
                 [msplit#2](x1, x2) = [1] x1 + [1]
                                                  
             [msplit#3](x1, x2, x3) = [1] x1 + [2]
                                                  
                              [#EQ] = [0]
                                         
                              [#GT] = [0]
                                         
                              [#LT] = [0]
                                         
                               [#0] = [2]
                                         
                         [#neg](x1) = [1] x1 + [0]
                                                  
                         [#pos](x1) = [1] x1 + [0]
                                                  
                           [#s](x1) = [1] x1 + [0]
                                                  
                  [#less^#](x1, x2) = [0]
                                         
                      [#cklt^#](x1) = [0]
                                         
               [#compare^#](x1, x2) = [0]
                                         
                  [merge^#](x1, x2) = [1] x1 + [0]
                                                  
                [merge#1^#](x1, x2) = [1] x1 + [0]
                                                  
            [merge#2^#](x1, x2, x3) = [1] x3 + [1]
                                                  
    [merge#3^#](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [1]
                                                           
                  [mergesort^#](x1) = [2] x1 + [0]
                                                  
                [mergesort#1^#](x1) = [2] x1 + [0]
                                                  
            [mergesort#2^#](x1, x2) = [2] x1 + [2]
                                                  
                [mergesort#3^#](x1) = [2] x1 + [0]
                                                  
                     [msplit^#](x1) = [0]
                                         
                   [msplit#1^#](x1) = [0]
                                         
               [msplit#2^#](x1, x2) = [0]
                                         
           [msplit#3^#](x1, x2, x3) = [0]
                                         
                          [c_1](x1) = [1] x1 + [0]
                                                  
                          [c_2](x1) = [1] x1 + [0]
                                                  
                          [c_3](x1) = [1] x1 + [0]
                                                  
                          [c_4](x1) = [1] x1 + [0]
                                                  
                          [c_5](x1) = [1] x1 + [0]
                                                  
                         [c_10](x1) = [1] x1 + [0]
                                                  
                         [c_11](x1) = [1] x1 + [0]
                                                  
                         [c_12](x1) = [1] x1 + [0]
  
  This order satisfies following ordering constraints
  
                            [#less(@x, @y)] =  [0]                                              
                                            >= [0]                                              
                                            =  [#cklt(#compare(@x, @y))]                        
                                                                                                
                     [#compare(#0(), #0())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#EQ()]                                          
                                                                                                
                 [#compare(#0(), #neg(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#GT()]                                          
                                                                                                
                 [#compare(#0(), #pos(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#LT()]                                          
                                                                                                
                   [#compare(#0(), #s(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#LT()]                                          
                                                                                                
                 [#compare(#neg(@x), #0())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#LT()]                                          
                                                                                                
             [#compare(#neg(@x), #neg(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#compare(@y, @x)]                               
                                                                                                
             [#compare(#neg(@x), #pos(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#LT()]                                          
                                                                                                
                 [#compare(#pos(@x), #0())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#GT()]                                          
                                                                                                
             [#compare(#pos(@x), #neg(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#GT()]                                          
                                                                                                
             [#compare(#pos(@x), #pos(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#compare(@x, @y)]                               
                                                                                                
                   [#compare(#s(@x), #0())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#GT()]                                          
                                                                                                
                 [#compare(#s(@x), #s(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#compare(@x, @y)]                               
                                                                                                
                             [#cklt(#EQ())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#false()]                                       
                                                                                                
                             [#cklt(#GT())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#false()]                                       
                                                                                                
                             [#cklt(#LT())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#true()]                                        
                                                                                                
                          [merge(@l1, @l2)] =  [1] @l1 + [1] @l2 + [0]                          
                                            >= [1] @l1 + [1] @l2 + [0]                          
                                            =  [merge#1(@l1, @l2)]                              
                                                                                                
                [merge#1(::(@x, @xs), @l2)] =  [1] @l2 + [1] @xs + [1]                          
                                            >= [1] @l2 + [1] @xs + [1]                          
                                            =  [merge#2(@l2, @x, @xs)]                          
                                                                                                
                      [merge#1(nil(), @l2)] =  [1] @l2 + [0]                                    
                                            >= [1] @l2 + [0]                                    
                                            =  [@l2]                                            
                                                                                                
            [merge#2(::(@y, @ys), @x, @xs)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [merge#3(#less(@x, @y), @x, @xs, @y, @ys)]       
                                                                                                
                  [merge#2(nil(), @x, @xs)] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [::(@x, @xs)]                                    
                                                                                                
      [merge#3(#false(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [::(@y, merge(::(@x, @xs), @ys))]                
                                                                                                
       [merge#3(#true(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [::(@x, merge(@xs, ::(@y, @ys)))]                
                                                                                                
                            [mergesort(@l)] =  [2] @l + [0]                                     
                                            >= [2] @l + [0]                                     
                                            =  [mergesort#1(@l)]                                
                                                                                                
                [mergesort#1(::(@x1, @xs))] =  [2] @xs + [2]                                    
                                            >= [2] @xs + [2]                                    
                                            =  [mergesort#2(@xs, @x1)]                          
                                                                                                
                       [mergesort#1(nil())] =  [0]                                              
                                            >= [0]                                              
                                            =  [nil()]                                          
                                                                                                
          [mergesort#2(::(@x2, @xs'), @x1)] =  [2] @xs' + [4]                                   
                                            >= [2] @xs' + [4]                                   
                                            =  [mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))]    
                                                                                                
                  [mergesort#2(nil(), @x1)] =  [2]                                              
                                            >  [1]                                              
                                            =  [::(@x1, nil())]                                 
                                                                                                
                               [msplit(@l)] =  [1] @l + [0]                                     
                                            >= [1] @l + [0]                                     
                                            =  [msplit#1(@l)]                                   
                                                                                                
           [mergesort#3(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l1 + [2] @l2 + [0]                          
                                            =  [merge(mergesort(@l1), mergesort(@l2))]          
                                                                                                
                   [msplit#1(::(@x1, @xs))] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [msplit#2(@xs, @x1)]                             
                                                                                                
                          [msplit#1(nil())] =  [0]                                              
                                            >= [0]                                              
                                            =  [tuple#2(nil(), nil())]                          
                                                                                                
             [msplit#2(::(@x2, @xs'), @x1)] =  [1] @xs' + [2]                                   
                                            >= [1] @xs' + [2]                                   
                                            =  [msplit#3(msplit(@xs'), @x1, @x2)]               
                                                                                                
                     [msplit#2(nil(), @x1)] =  [1]                                              
                                            >= [1]                                              
                                            =  [tuple#2(::(@x1, nil()), nil())]                 
                                                                                                
    [msplit#3(tuple#2(@l1, @l2), @x1, @x2)] =  [1] @l1 + [1] @l2 + [2]                          
                                            >= [1] @l1 + [1] @l2 + [2]                          
                                            =  [tuple#2(::(@x1, @l1), ::(@x2, @l2))]            
                                                                                                
                        [merge^#(@l1, @l2)] =  [1] @l1 + [0]                                    
                                            >= [1] @l1 + [0]                                    
                                            =  [c_1(merge#1^#(@l1, @l2))]                       
                                                                                                
              [merge#1^#(::(@x, @xs), @l2)] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [c_2(merge#2^#(@l2, @x, @xs))]                   
                                                                                                
          [merge#2^#(::(@y, @ys), @x, @xs)] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))]
                                                                                                
    [merge#3^#(#false(), @x, @xs, @y, @ys)] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [c_4(merge^#(::(@x, @xs), @ys))]                 
                                                                                                
     [merge#3^#(#true(), @x, @xs, @y, @ys)] =  [1] @xs + [1]                                    
                                            >  [1] @xs + [0]                                    
                                            =  [c_5(merge^#(@xs, ::(@y, @ys)))]                 
                                                                                                
                          [mergesort^#(@l)] =  [2] @l + [0]                                     
                                            >= [2] @l + [0]                                     
                                            =  [mergesort#1^#(@l)]                              
                                                                                                
              [mergesort#1^#(::(@x1, @xs))] =  [2] @xs + [2]                                    
                                            >= [2] @xs + [2]                                    
                                            =  [mergesort#2^#(@xs, @x1)]                        
                                                                                                
        [mergesort#2^#(::(@x2, @xs'), @x1)] =  [2] @xs' + [4]                                   
                                            >= [2] @xs' + [4]                                   
                                            =  [mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))]  
                                                                                                
        [mergesort#2^#(::(@x2, @xs'), @x1)] =  [2] @xs' + [4]                                   
                                            >  [0]                                              
                                            =  [msplit^#(::(@x1, ::(@x2, @xs')))]               
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l1 + [0]                                    
                                            =  [merge^#(mergesort(@l1), mergesort(@l2))]        
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l1 + [0]                                    
                                            =  [mergesort^#(@l1)]                               
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l2 + [0]                                    
                                            =  [mergesort^#(@l2)]                               
                                                                                                
                             [msplit^#(@l)] =  [0]                                              
                                            >= [0]                                              
                                            =  [c_10(msplit#1^#(@l))]                           
                                                                                                
                 [msplit#1^#(::(@x1, @xs))] =  [0]                                              
                                            >= [0]                                              
                                            =  [c_11(msplit#2^#(@xs, @x1))]                     
                                                                                                
           [msplit#2^#(::(@x2, @xs'), @x1)] =  [0]                                              
                                            >= [0]                                              
                                            =  [c_12(msplit^#(@xs'))]                           
                                                                                                

The strictly oriented rules are moved into the corresponding weak
component(s).


We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys))
  , msplit^#(@l) -> c_10(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_11(msplit#2^#(@xs, @x1))
  , msplit#2^#(::(@x2, @xs'), @x1) -> c_12(msplit^#(@xs')) }
Weak DPs:
  { merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> mergesort#1^#(@l)
  , mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    msplit^#(::(@x1, ::(@x2, @xs')))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    merge^#(mergesort(@l1), mergesort(@l2))
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 5: msplit^#(@l) -> c_10(msplit#1^#(@l))
  , 6: msplit#1^#(::(@x1, @xs)) -> c_11(msplit#2^#(@xs, @x1)) }
Trs:
  { mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs')))) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
    Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_10) = {1},
    Uargs(c_11) = {1}, Uargs(c_12) = {1}
  
  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).
  
                    [#less](x1, x2) = [0]
                                         
                 [#compare](x1, x2) = [0]
                                         
                        [#cklt](x1) = [0]
                                         
                    [merge](x1, x2) = [1] x2 + [2]
                                                  
                  [merge#1](x1, x2) = [1] x1 + [2] x2 + [0]
                                                           
                       [::](x1, x2) = [1] x2 + [1]
                                                  
              [merge#2](x1, x2, x3) = [2] x2 + [2] x3 + [0]
                                                           
                              [nil] = [0]
                                         
      [merge#3](x1, x2, x3, x4, x5) = [2] x3 + [1] x5 + [2]
                                                           
                           [#false] = [0]
                                         
                            [#true] = [0]
                                         
                    [mergesort](x1) = [0]
                                         
                  [mergesort#1](x1) = [0]
                                         
              [mergesort#2](x1, x2) = [2] x2 + [1]
                                                  
                       [msplit](x1) = [1] x1 + [1]
                                                  
                  [mergesort#3](x1) = [0]
                                         
                  [tuple#2](x1, x2) = [1] x1 + [1] x2 + [1]
                                                           
                     [msplit#1](x1) = [1] x1 + [1]
                                                  
                 [msplit#2](x1, x2) = [1] x1 + [2]
                                                  
             [msplit#3](x1, x2, x3) = [1] x1 + [2]
                                                  
                              [#EQ] = [0]
                                         
                              [#GT] = [0]
                                         
                              [#LT] = [0]
                                         
                               [#0] = [0]
                                         
                         [#neg](x1) = [1] x1 + [0]
                                                  
                         [#pos](x1) = [1] x1 + [0]
                                                  
                           [#s](x1) = [1] x1 + [0]
                                                  
                  [#less^#](x1, x2) = [0]
                                         
                      [#cklt^#](x1) = [0]
                                         
               [#compare^#](x1, x2) = [0]
                                         
                  [merge^#](x1, x2) = [1]
                                         
                [merge#1^#](x1, x2) = [1]
                                         
            [merge#2^#](x1, x2, x3) = [1]
                                         
    [merge#3^#](x1, x2, x3, x4, x5) = [1]
                                         
                  [mergesort^#](x1) = [1] x1 + [1]
                                                  
                [mergesort#1^#](x1) = [1] x1 + [1]
                                                  
            [mergesort#2^#](x1, x2) = [1] x1 + [2]
                                                  
                [mergesort#3^#](x1) = [1] x1 + [0]
                                                  
                     [msplit^#](x1) = [1] x1 + [1]
                                                  
                   [msplit#1^#](x1) = [1] x1 + [0]
                                                  
               [msplit#2^#](x1, x2) = [1] x1 + [0]
                                                  
           [msplit#3^#](x1, x2, x3) = [0]
                                         
                          [c_1](x1) = [1] x1 + [0]
                                                  
                          [c_2](x1) = [1] x1 + [0]
                                                  
                          [c_3](x1) = [1] x1 + [0]
                                                  
                          [c_4](x1) = [1] x1 + [0]
                                                  
                          [c_5](x1) = [1] x1 + [0]
                                                  
                         [c_10](x1) = [1] x1 + [0]
                                                  
                         [c_11](x1) = [1] x1 + [0]
                                                  
                         [c_12](x1) = [1] x1 + [0]
  
  This order satisfies following ordering constraints
  
                               [msplit(@l)] =  [1] @l + [1]                                     
                                            >= [1] @l + [1]                                     
                                            =  [msplit#1(@l)]                                   
                                                                                                
                   [msplit#1(::(@x1, @xs))] =  [1] @xs + [2]                                    
                                            >= [1] @xs + [2]                                    
                                            =  [msplit#2(@xs, @x1)]                             
                                                                                                
                          [msplit#1(nil())] =  [1]                                              
                                            >= [1]                                              
                                            =  [tuple#2(nil(), nil())]                          
                                                                                                
             [msplit#2(::(@x2, @xs'), @x1)] =  [1] @xs' + [3]                                   
                                            >= [1] @xs' + [3]                                   
                                            =  [msplit#3(msplit(@xs'), @x1, @x2)]               
                                                                                                
                     [msplit#2(nil(), @x1)] =  [2]                                              
                                            >= [2]                                              
                                            =  [tuple#2(::(@x1, nil()), nil())]                 
                                                                                                
    [msplit#3(tuple#2(@l1, @l2), @x1, @x2)] =  [1] @l1 + [1] @l2 + [3]                          
                                            >= [1] @l1 + [1] @l2 + [3]                          
                                            =  [tuple#2(::(@x1, @l1), ::(@x2, @l2))]            
                                                                                                
                        [merge^#(@l1, @l2)] =  [1]                                              
                                            >= [1]                                              
                                            =  [c_1(merge#1^#(@l1, @l2))]                       
                                                                                                
              [merge#1^#(::(@x, @xs), @l2)] =  [1]                                              
                                            >= [1]                                              
                                            =  [c_2(merge#2^#(@l2, @x, @xs))]                   
                                                                                                
          [merge#2^#(::(@y, @ys), @x, @xs)] =  [1]                                              
                                            >= [1]                                              
                                            =  [c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))]
                                                                                                
    [merge#3^#(#false(), @x, @xs, @y, @ys)] =  [1]                                              
                                            >= [1]                                              
                                            =  [c_4(merge^#(::(@x, @xs), @ys))]                 
                                                                                                
     [merge#3^#(#true(), @x, @xs, @y, @ys)] =  [1]                                              
                                            >= [1]                                              
                                            =  [c_5(merge^#(@xs, ::(@y, @ys)))]                 
                                                                                                
                          [mergesort^#(@l)] =  [1] @l + [1]                                     
                                            >= [1] @l + [1]                                     
                                            =  [mergesort#1^#(@l)]                              
                                                                                                
              [mergesort#1^#(::(@x1, @xs))] =  [1] @xs + [2]                                    
                                            >= [1] @xs + [2]                                    
                                            =  [mergesort#2^#(@xs, @x1)]                        
                                                                                                
        [mergesort#2^#(::(@x2, @xs'), @x1)] =  [1] @xs' + [3]                                   
                                            >= [1] @xs' + [3]                                   
                                            =  [mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))]  
                                                                                                
        [mergesort#2^#(::(@x2, @xs'), @x1)] =  [1] @xs' + [3]                                   
                                            >= [1] @xs' + [3]                                   
                                            =  [msplit^#(::(@x1, ::(@x2, @xs')))]               
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [1]                          
                                            >= [1]                                              
                                            =  [merge^#(mergesort(@l1), mergesort(@l2))]        
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [1]                          
                                            >= [1] @l1 + [1]                                    
                                            =  [mergesort^#(@l1)]                               
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [1]                          
                                            >= [1] @l2 + [1]                                    
                                            =  [mergesort^#(@l2)]                               
                                                                                                
                             [msplit^#(@l)] =  [1] @l + [1]                                     
                                            >  [1] @l + [0]                                     
                                            =  [c_10(msplit#1^#(@l))]                           
                                                                                                
                 [msplit#1^#(::(@x1, @xs))] =  [1] @xs + [1]                                    
                                            >  [1] @xs + [0]                                    
                                            =  [c_11(msplit#2^#(@xs, @x1))]                     
                                                                                                
           [msplit#2^#(::(@x2, @xs'), @x1)] =  [1] @xs' + [1]                                   
                                            >= [1] @xs' + [1]                                   
                                            =  [c_12(msplit^#(@xs'))]                           
                                                                                                

Consider the set of all dependency pairs

DPs:
  { 1: merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , 2: merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , 3: merge#2^#(::(@y, @ys), @x, @xs) ->
       c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , 4: merge#3^#(#false(), @x, @xs, @y, @ys) ->
       c_4(merge^#(::(@x, @xs), @ys))
  , 5: msplit^#(@l) -> c_10(msplit#1^#(@l))
  , 6: msplit#1^#(::(@x1, @xs)) -> c_11(msplit#2^#(@xs, @x1))
  , 7: msplit#2^#(::(@x2, @xs'), @x1) -> c_12(msplit^#(@xs'))
  , 8: merge#3^#(#true(), @x, @xs, @y, @ys) ->
       c_5(merge^#(@xs, ::(@y, @ys)))
  , 9: mergesort^#(@l) -> mergesort#1^#(@l)
  , 10: mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , 11: mergesort#2^#(::(@x2, @xs'), @x1) ->
        mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , 12: mergesort#2^#(::(@x2, @xs'), @x1) ->
        msplit^#(::(@x1, ::(@x2, @xs')))
  , 13: mergesort#3^#(tuple#2(@l1, @l2)) ->
        merge^#(mergesort(@l1), mergesort(@l2))
  , 14: mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , 15: mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {5,6}. These cover all (indirect) predecessors of dependency
pairs {5,6,7}, their number of application is equally bounded. The
dependency pairs are shifted into the corresponding weak
component(s).

We apply the transformation 'removetails' on the sub-problem:

Strict DPs:
  { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys)) }
Weak DPs:
  { merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> mergesort#1^#(@l)
  , mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    msplit^#(::(@x1, ::(@x2, @xs')))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    merge^#(mergesort(@l1), mergesort(@l2))
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2)
  , msplit^#(@l) -> c_10(msplit#1^#(@l))
  , msplit#1^#(::(@x1, @xs)) -> c_11(msplit#2^#(@xs, @x1))
  , msplit#2^#(::(@x2, @xs'), @x1) -> c_12(msplit^#(@xs')) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
StartTerms: basic terms
Strategy: innermost

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ mergesort#2^#(::(@x2, @xs'), @x1) ->
  msplit^#(::(@x1, ::(@x2, @xs')))
, msplit^#(@l) -> c_10(msplit#1^#(@l))
, msplit#1^#(::(@x1, @xs)) -> c_11(msplit#2^#(@xs, @x1))
, msplit#2^#(::(@x2, @xs'), @x1) -> c_12(msplit^#(@xs')) }



We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys)) }
Weak DPs:
  { merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> mergesort#1^#(@l)
  , mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    merge^#(mergesort(@l1), mergesort(@l2))
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 3: merge#2^#(::(@y, @ys), @x, @xs) ->
       c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , 5: merge#3^#(#true(), @x, @xs, @y, @ys) ->
       c_5(merge^#(@xs, ::(@y, @ys))) }
Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
    Uargs(c_4) = {1}, Uargs(c_5) = {1}
  
  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).
  
                    [#less](x1, x2) = [1]
                                         
                 [#compare](x1, x2) = [0]
                                         
                        [#cklt](x1) = [0]
                                         
                    [merge](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                  [merge#1](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                       [::](x1, x2) = [1] x2 + [1]
                                                  
              [merge#2](x1, x2, x3) = [1] x1 + [1] x3 + [1]
                                                           
                              [nil] = [0]
                                         
      [merge#3](x1, x2, x3, x4, x5) = [1] x3 + [1] x5 + [2]
                                                           
                           [#false] = [0]
                                         
                            [#true] = [0]
                                         
                    [mergesort](x1) = [1] x1 + [0]
                                                  
                  [mergesort#1](x1) = [1] x1 + [0]
                                                  
              [mergesort#2](x1, x2) = [1] x1 + [1]
                                                  
                       [msplit](x1) = [1] x1 + [0]
                                                  
                  [mergesort#3](x1) = [1] x1 + [0]
                                                  
                  [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                     [msplit#1](x1) = [1] x1 + [0]
                                                  
                 [msplit#2](x1, x2) = [1] x1 + [1]
                                                  
             [msplit#3](x1, x2, x3) = [1] x1 + [2]
                                                  
                              [#EQ] = [0]
                                         
                              [#GT] = [0]
                                         
                              [#LT] = [0]
                                         
                               [#0] = [0]
                                         
                         [#neg](x1) = [1] x1 + [0]
                                                  
                         [#pos](x1) = [1] x1 + [0]
                                                  
                           [#s](x1) = [1] x1 + [0]
                                                  
                  [#less^#](x1, x2) = [0]
                                         
                      [#cklt^#](x1) = [0]
                                         
               [#compare^#](x1, x2) = [0]
                                         
                  [merge^#](x1, x2) = [2] x1 + [1] x2 + [0]
                                                           
                [merge#1^#](x1, x2) = [2] x1 + [1] x2 + [0]
                                                           
            [merge#2^#](x1, x2, x3) = [1] x1 + [2] x3 + [2]
                                                           
    [merge#3^#](x1, x2, x3, x4, x5) = [2] x3 + [1] x5 + [2]
                                                           
                  [mergesort^#](x1) = [2] x1 + [0]
                                                  
                [mergesort#1^#](x1) = [2] x1 + [0]
                                                  
            [mergesort#2^#](x1, x2) = [2] x1 + [2]
                                                  
                [mergesort#3^#](x1) = [2] x1 + [0]
                                                  
                     [msplit^#](x1) = [0]
                                         
                   [msplit#1^#](x1) = [0]
                                         
               [msplit#2^#](x1, x2) = [0]
                                         
           [msplit#3^#](x1, x2, x3) = [0]
                                         
                          [c_1](x1) = [1] x1 + [0]
                                                  
                          [c_2](x1) = [1] x1 + [0]
                                                  
                          [c_3](x1) = [1] x1 + [0]
                                                  
                          [c_4](x1) = [1] x1 + [0]
                                                  
                          [c_5](x1) = [1] x1 + [0]
                                                  
                         [c_10](x1) = [0]
                                         
                         [c_11](x1) = [0]
                                         
                         [c_12](x1) = [0]
  
  This order satisfies following ordering constraints
  
                          [merge(@l1, @l2)] =  [1] @l1 + [1] @l2 + [0]                          
                                            >= [1] @l1 + [1] @l2 + [0]                          
                                            =  [merge#1(@l1, @l2)]                              
                                                                                                
                [merge#1(::(@x, @xs), @l2)] =  [1] @l2 + [1] @xs + [1]                          
                                            >= [1] @l2 + [1] @xs + [1]                          
                                            =  [merge#2(@l2, @x, @xs)]                          
                                                                                                
                      [merge#1(nil(), @l2)] =  [1] @l2 + [0]                                    
                                            >= [1] @l2 + [0]                                    
                                            =  [@l2]                                            
                                                                                                
            [merge#2(::(@y, @ys), @x, @xs)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [merge#3(#less(@x, @y), @x, @xs, @y, @ys)]       
                                                                                                
                  [merge#2(nil(), @x, @xs)] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [::(@x, @xs)]                                    
                                                                                                
      [merge#3(#false(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [::(@y, merge(::(@x, @xs), @ys))]                
                                                                                                
       [merge#3(#true(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [::(@x, merge(@xs, ::(@y, @ys)))]                
                                                                                                
                            [mergesort(@l)] =  [1] @l + [0]                                     
                                            >= [1] @l + [0]                                     
                                            =  [mergesort#1(@l)]                                
                                                                                                
                [mergesort#1(::(@x1, @xs))] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [mergesort#2(@xs, @x1)]                          
                                                                                                
                       [mergesort#1(nil())] =  [0]                                              
                                            >= [0]                                              
                                            =  [nil()]                                          
                                                                                                
          [mergesort#2(::(@x2, @xs'), @x1)] =  [1] @xs' + [2]                                   
                                            >= [1] @xs' + [2]                                   
                                            =  [mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))]    
                                                                                                
                  [mergesort#2(nil(), @x1)] =  [1]                                              
                                            >= [1]                                              
                                            =  [::(@x1, nil())]                                 
                                                                                                
                               [msplit(@l)] =  [1] @l + [0]                                     
                                            >= [1] @l + [0]                                     
                                            =  [msplit#1(@l)]                                   
                                                                                                
           [mergesort#3(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [0]                          
                                            >= [1] @l1 + [1] @l2 + [0]                          
                                            =  [merge(mergesort(@l1), mergesort(@l2))]          
                                                                                                
                   [msplit#1(::(@x1, @xs))] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [msplit#2(@xs, @x1)]                             
                                                                                                
                          [msplit#1(nil())] =  [0]                                              
                                            >= [0]                                              
                                            =  [tuple#2(nil(), nil())]                          
                                                                                                
             [msplit#2(::(@x2, @xs'), @x1)] =  [1] @xs' + [2]                                   
                                            >= [1] @xs' + [2]                                   
                                            =  [msplit#3(msplit(@xs'), @x1, @x2)]               
                                                                                                
                     [msplit#2(nil(), @x1)] =  [1]                                              
                                            >= [1]                                              
                                            =  [tuple#2(::(@x1, nil()), nil())]                 
                                                                                                
    [msplit#3(tuple#2(@l1, @l2), @x1, @x2)] =  [1] @l1 + [1] @l2 + [2]                          
                                            >= [1] @l1 + [1] @l2 + [2]                          
                                            =  [tuple#2(::(@x1, @l1), ::(@x2, @l2))]            
                                                                                                
                        [merge^#(@l1, @l2)] =  [2] @l1 + [1] @l2 + [0]                          
                                            >= [2] @l1 + [1] @l2 + [0]                          
                                            =  [c_1(merge#1^#(@l1, @l2))]                       
                                                                                                
              [merge#1^#(::(@x, @xs), @l2)] =  [1] @l2 + [2] @xs + [2]                          
                                            >= [1] @l2 + [2] @xs + [2]                          
                                            =  [c_2(merge#2^#(@l2, @x, @xs))]                   
                                                                                                
          [merge#2^#(::(@y, @ys), @x, @xs)] =  [2] @xs + [1] @ys + [3]                          
                                            >  [2] @xs + [1] @ys + [2]                          
                                            =  [c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))]
                                                                                                
    [merge#3^#(#false(), @x, @xs, @y, @ys)] =  [2] @xs + [1] @ys + [2]                          
                                            >= [2] @xs + [1] @ys + [2]                          
                                            =  [c_4(merge^#(::(@x, @xs), @ys))]                 
                                                                                                
     [merge#3^#(#true(), @x, @xs, @y, @ys)] =  [2] @xs + [1] @ys + [2]                          
                                            >  [2] @xs + [1] @ys + [1]                          
                                            =  [c_5(merge^#(@xs, ::(@y, @ys)))]                 
                                                                                                
                          [mergesort^#(@l)] =  [2] @l + [0]                                     
                                            >= [2] @l + [0]                                     
                                            =  [mergesort#1^#(@l)]                              
                                                                                                
              [mergesort#1^#(::(@x1, @xs))] =  [2] @xs + [2]                                    
                                            >= [2] @xs + [2]                                    
                                            =  [mergesort#2^#(@xs, @x1)]                        
                                                                                                
        [mergesort#2^#(::(@x2, @xs'), @x1)] =  [2] @xs' + [4]                                   
                                            >= [2] @xs' + [4]                                   
                                            =  [mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))]  
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l1 + [1] @l2 + [0]                          
                                            =  [merge^#(mergesort(@l1), mergesort(@l2))]        
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l1 + [0]                                    
                                            =  [mergesort^#(@l1)]                               
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l2 + [0]                                    
                                            =  [mergesort^#(@l2)]                               
                                                                                                

Consider the set of all dependency pairs

DPs:
  { 1: merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , 2: merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , 3: merge#2^#(::(@y, @ys), @x, @xs) ->
       c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , 4: merge#3^#(#false(), @x, @xs, @y, @ys) ->
       c_4(merge^#(::(@x, @xs), @ys))
  , 5: merge#3^#(#true(), @x, @xs, @y, @ys) ->
       c_5(merge^#(@xs, ::(@y, @ys)))
  , 6: mergesort^#(@l) -> mergesort#1^#(@l)
  , 7: mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , 8: mergesort#2^#(::(@x2, @xs'), @x1) ->
       mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , 9: mergesort#3^#(tuple#2(@l1, @l2)) ->
       merge^#(mergesort(@l1), mergesort(@l2))
  , 10: mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , 11: mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {3,5}. These cover all (indirect) predecessors of dependency
pairs {3,4,5}, their number of application is equally bounded. The
dependency pairs are shifted into the corresponding weak
component(s).


We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs)) }
Weak DPs:
  { merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> mergesort#1^#(@l)
  , mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    merge^#(mergesort(@l1), mergesort(@l2))
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 2: merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
    Uargs(c_4) = {1}, Uargs(c_5) = {1}
  
  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).
  
                    [#less](x1, x2) = [1]
                                         
                 [#compare](x1, x2) = [1]
                                         
                        [#cklt](x1) = [1] x1 + [0]
                                                  
                    [merge](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                  [merge#1](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                       [::](x1, x2) = [1] x2 + [1]
                                                  
              [merge#2](x1, x2, x3) = [1] x1 + [1] x3 + [1]
                                                           
                              [nil] = [0]
                                         
      [merge#3](x1, x2, x3, x4, x5) = [1] x3 + [1] x5 + [2]
                                                           
                           [#false] = [1]
                                         
                            [#true] = [1]
                                         
                    [mergesort](x1) = [1] x1 + [0]
                                                  
                  [mergesort#1](x1) = [1] x1 + [0]
                                                  
              [mergesort#2](x1, x2) = [1] x1 + [1]
                                                  
                       [msplit](x1) = [1] x1 + [0]
                                                  
                  [mergesort#3](x1) = [1] x1 + [0]
                                                  
                  [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                     [msplit#1](x1) = [1] x1 + [0]
                                                  
                 [msplit#2](x1, x2) = [1] x1 + [1]
                                                  
             [msplit#3](x1, x2, x3) = [1] x1 + [2]
                                                  
                              [#EQ] = [1]
                                         
                              [#GT] = [1]
                                         
                              [#LT] = [1]
                                         
                               [#0] = [1]
                                         
                         [#neg](x1) = [1] x1 + [0]
                                                  
                         [#pos](x1) = [1] x1 + [0]
                                                  
                           [#s](x1) = [1] x1 + [0]
                                                  
                  [#less^#](x1, x2) = [0]
                                         
                      [#cklt^#](x1) = [0]
                                         
               [#compare^#](x1, x2) = [0]
                                         
                  [merge^#](x1, x2) = [1] x1 + [2] x2 + [0]
                                                           
                [merge#1^#](x1, x2) = [1] x1 + [2] x2 + [0]
                                                           
            [merge#2^#](x1, x2, x3) = [2] x1 + [1] x3 + [0]
                                                           
    [merge#3^#](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [2] x5 + [1]
                                                                    
                  [mergesort^#](x1) = [2] x1 + [0]
                                                  
                [mergesort#1^#](x1) = [2] x1 + [0]
                                                  
            [mergesort#2^#](x1, x2) = [2] x1 + [2]
                                                  
                [mergesort#3^#](x1) = [2] x1 + [0]
                                                  
                     [msplit^#](x1) = [0]
                                         
                   [msplit#1^#](x1) = [0]
                                         
               [msplit#2^#](x1, x2) = [0]
                                         
           [msplit#3^#](x1, x2, x3) = [0]
                                         
                          [c_1](x1) = [1] x1 + [0]
                                                  
                          [c_2](x1) = [1] x1 + [0]
                                                  
                          [c_3](x1) = [1] x1 + [0]
                                                  
                          [c_4](x1) = [1] x1 + [1]
                                                  
                          [c_5](x1) = [1] x1 + [0]
                                                  
                         [c_10](x1) = [0]
                                         
                         [c_11](x1) = [0]
                                         
                         [c_12](x1) = [0]
  
  This order satisfies following ordering constraints
  
                            [#less(@x, @y)] =  [1]                                              
                                            >= [1]                                              
                                            =  [#cklt(#compare(@x, @y))]                        
                                                                                                
                     [#compare(#0(), #0())] =  [1]                                              
                                            >= [1]                                              
                                            =  [#EQ()]                                          
                                                                                                
                 [#compare(#0(), #neg(@y))] =  [1]                                              
                                            >= [1]                                              
                                            =  [#GT()]                                          
                                                                                                
                 [#compare(#0(), #pos(@y))] =  [1]                                              
                                            >= [1]                                              
                                            =  [#LT()]                                          
                                                                                                
                   [#compare(#0(), #s(@y))] =  [1]                                              
                                            >= [1]                                              
                                            =  [#LT()]                                          
                                                                                                
                 [#compare(#neg(@x), #0())] =  [1]                                              
                                            >= [1]                                              
                                            =  [#LT()]                                          
                                                                                                
             [#compare(#neg(@x), #neg(@y))] =  [1]                                              
                                            >= [1]                                              
                                            =  [#compare(@y, @x)]                               
                                                                                                
             [#compare(#neg(@x), #pos(@y))] =  [1]                                              
                                            >= [1]                                              
                                            =  [#LT()]                                          
                                                                                                
                 [#compare(#pos(@x), #0())] =  [1]                                              
                                            >= [1]                                              
                                            =  [#GT()]                                          
                                                                                                
             [#compare(#pos(@x), #neg(@y))] =  [1]                                              
                                            >= [1]                                              
                                            =  [#GT()]                                          
                                                                                                
             [#compare(#pos(@x), #pos(@y))] =  [1]                                              
                                            >= [1]                                              
                                            =  [#compare(@x, @y)]                               
                                                                                                
                   [#compare(#s(@x), #0())] =  [1]                                              
                                            >= [1]                                              
                                            =  [#GT()]                                          
                                                                                                
                 [#compare(#s(@x), #s(@y))] =  [1]                                              
                                            >= [1]                                              
                                            =  [#compare(@x, @y)]                               
                                                                                                
                             [#cklt(#EQ())] =  [1]                                              
                                            >= [1]                                              
                                            =  [#false()]                                       
                                                                                                
                             [#cklt(#GT())] =  [1]                                              
                                            >= [1]                                              
                                            =  [#false()]                                       
                                                                                                
                             [#cklt(#LT())] =  [1]                                              
                                            >= [1]                                              
                                            =  [#true()]                                        
                                                                                                
                          [merge(@l1, @l2)] =  [1] @l1 + [1] @l2 + [0]                          
                                            >= [1] @l1 + [1] @l2 + [0]                          
                                            =  [merge#1(@l1, @l2)]                              
                                                                                                
                [merge#1(::(@x, @xs), @l2)] =  [1] @l2 + [1] @xs + [1]                          
                                            >= [1] @l2 + [1] @xs + [1]                          
                                            =  [merge#2(@l2, @x, @xs)]                          
                                                                                                
                      [merge#1(nil(), @l2)] =  [1] @l2 + [0]                                    
                                            >= [1] @l2 + [0]                                    
                                            =  [@l2]                                            
                                                                                                
            [merge#2(::(@y, @ys), @x, @xs)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [merge#3(#less(@x, @y), @x, @xs, @y, @ys)]       
                                                                                                
                  [merge#2(nil(), @x, @xs)] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [::(@x, @xs)]                                    
                                                                                                
      [merge#3(#false(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [::(@y, merge(::(@x, @xs), @ys))]                
                                                                                                
       [merge#3(#true(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [::(@x, merge(@xs, ::(@y, @ys)))]                
                                                                                                
                            [mergesort(@l)] =  [1] @l + [0]                                     
                                            >= [1] @l + [0]                                     
                                            =  [mergesort#1(@l)]                                
                                                                                                
                [mergesort#1(::(@x1, @xs))] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [mergesort#2(@xs, @x1)]                          
                                                                                                
                       [mergesort#1(nil())] =  [0]                                              
                                            >= [0]                                              
                                            =  [nil()]                                          
                                                                                                
          [mergesort#2(::(@x2, @xs'), @x1)] =  [1] @xs' + [2]                                   
                                            >= [1] @xs' + [2]                                   
                                            =  [mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))]    
                                                                                                
                  [mergesort#2(nil(), @x1)] =  [1]                                              
                                            >= [1]                                              
                                            =  [::(@x1, nil())]                                 
                                                                                                
                               [msplit(@l)] =  [1] @l + [0]                                     
                                            >= [1] @l + [0]                                     
                                            =  [msplit#1(@l)]                                   
                                                                                                
           [mergesort#3(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [0]                          
                                            >= [1] @l1 + [1] @l2 + [0]                          
                                            =  [merge(mergesort(@l1), mergesort(@l2))]          
                                                                                                
                   [msplit#1(::(@x1, @xs))] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [msplit#2(@xs, @x1)]                             
                                                                                                
                          [msplit#1(nil())] =  [0]                                              
                                            >= [0]                                              
                                            =  [tuple#2(nil(), nil())]                          
                                                                                                
             [msplit#2(::(@x2, @xs'), @x1)] =  [1] @xs' + [2]                                   
                                            >= [1] @xs' + [2]                                   
                                            =  [msplit#3(msplit(@xs'), @x1, @x2)]               
                                                                                                
                     [msplit#2(nil(), @x1)] =  [1]                                              
                                            >= [1]                                              
                                            =  [tuple#2(::(@x1, nil()), nil())]                 
                                                                                                
    [msplit#3(tuple#2(@l1, @l2), @x1, @x2)] =  [1] @l1 + [1] @l2 + [2]                          
                                            >= [1] @l1 + [1] @l2 + [2]                          
                                            =  [tuple#2(::(@x1, @l1), ::(@x2, @l2))]            
                                                                                                
                        [merge^#(@l1, @l2)] =  [1] @l1 + [2] @l2 + [0]                          
                                            >= [1] @l1 + [2] @l2 + [0]                          
                                            =  [c_1(merge#1^#(@l1, @l2))]                       
                                                                                                
              [merge#1^#(::(@x, @xs), @l2)] =  [2] @l2 + [1] @xs + [1]                          
                                            >  [2] @l2 + [1] @xs + [0]                          
                                            =  [c_2(merge#2^#(@l2, @x, @xs))]                   
                                                                                                
          [merge#2^#(::(@y, @ys), @x, @xs)] =  [1] @xs + [2] @ys + [2]                          
                                            >= [1] @xs + [2] @ys + [2]                          
                                            =  [c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))]
                                                                                                
    [merge#3^#(#false(), @x, @xs, @y, @ys)] =  [1] @xs + [2] @ys + [2]                          
                                            >= [1] @xs + [2] @ys + [2]                          
                                            =  [c_4(merge^#(::(@x, @xs), @ys))]                 
                                                                                                
     [merge#3^#(#true(), @x, @xs, @y, @ys)] =  [1] @xs + [2] @ys + [2]                          
                                            >= [1] @xs + [2] @ys + [2]                          
                                            =  [c_5(merge^#(@xs, ::(@y, @ys)))]                 
                                                                                                
                          [mergesort^#(@l)] =  [2] @l + [0]                                     
                                            >= [2] @l + [0]                                     
                                            =  [mergesort#1^#(@l)]                              
                                                                                                
              [mergesort#1^#(::(@x1, @xs))] =  [2] @xs + [2]                                    
                                            >= [2] @xs + [2]                                    
                                            =  [mergesort#2^#(@xs, @x1)]                        
                                                                                                
        [mergesort#2^#(::(@x2, @xs'), @x1)] =  [2] @xs' + [4]                                   
                                            >= [2] @xs' + [4]                                   
                                            =  [mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))]  
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [1] @l1 + [2] @l2 + [0]                          
                                            =  [merge^#(mergesort(@l1), mergesort(@l2))]        
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l1 + [0]                                    
                                            =  [mergesort^#(@l1)]                               
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [2] @l1 + [2] @l2 + [0]                          
                                            >= [2] @l2 + [0]                                    
                                            =  [mergesort^#(@l2)]                               
                                                                                                

Consider the set of all dependency pairs

DPs:
  { 1: merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , 2: merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , 3: merge#2^#(::(@y, @ys), @x, @xs) ->
       c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , 4: merge#3^#(#false(), @x, @xs, @y, @ys) ->
       c_4(merge^#(::(@x, @xs), @ys))
  , 5: merge#3^#(#true(), @x, @xs, @y, @ys) ->
       c_5(merge^#(@xs, ::(@y, @ys)))
  , 6: mergesort^#(@l) -> mergesort#1^#(@l)
  , 7: mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , 8: mergesort#2^#(::(@x2, @xs'), @x1) ->
       mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , 9: mergesort#3^#(tuple#2(@l1, @l2)) ->
       merge^#(mergesort(@l1), mergesort(@l2))
  , 10: mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , 11: mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2}. These cover all (indirect) predecessors of dependency
pairs {2,3,4,5}, their number of application is equally bounded.
The dependency pairs are shifted into the corresponding weak
component(s).


We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs: { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2)) }
Weak DPs:
  { merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> mergesort#1^#(@l)
  , mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    merge^#(mergesort(@l1), mergesort(@l2))
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 2: merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , 9: mergesort#3^#(tuple#2(@l1, @l2)) ->
       merge^#(mergesort(@l1), mergesort(@l2)) }
Trs: { #cklt(#LT()) -> #true() }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
    Uargs(c_4) = {1}, Uargs(c_5) = {1}
  
  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).
  
                    [#less](x1, x2) = [1]
                                         
                 [#compare](x1, x2) = [0]
                                         
                        [#cklt](x1) = [1] x1 + [1]
                                                  
                    [merge](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                  [merge#1](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                       [::](x1, x2) = [1] x2 + [1]
                                                  
              [merge#2](x1, x2, x3) = [1] x1 + [1] x3 + [1]
                                                           
                              [nil] = [0]
                                         
      [merge#3](x1, x2, x3, x4, x5) = [1] x3 + [1] x5 + [2]
                                                           
                           [#false] = [1]
                                         
                            [#true] = [0]
                                         
                    [mergesort](x1) = [1] x1 + [0]
                                                  
                  [mergesort#1](x1) = [1] x1 + [0]
                                                  
              [mergesort#2](x1, x2) = [1] x1 + [1]
                                                  
                       [msplit](x1) = [1] x1 + [0]
                                                  
                  [mergesort#3](x1) = [1] x1 + [0]
                                                  
                  [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                     [msplit#1](x1) = [1] x1 + [0]
                                                  
                 [msplit#2](x1, x2) = [1] x1 + [1]
                                                  
             [msplit#3](x1, x2, x3) = [1] x1 + [2]
                                                  
                              [#EQ] = [0]
                                         
                              [#GT] = [0]
                                         
                              [#LT] = [0]
                                         
                               [#0] = [0]
                                         
                         [#neg](x1) = [1] x1 + [0]
                                                  
                         [#pos](x1) = [1] x1 + [0]
                                                  
                           [#s](x1) = [1] x1 + [1]
                                                  
                  [#less^#](x1, x2) = [0]
                                         
                      [#cklt^#](x1) = [0]
                                         
               [#compare^#](x1, x2) = [0]
                                         
                  [merge^#](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
                [merge#1^#](x1, x2) = [1] x1 + [1] x2 + [0]
                                                           
            [merge#2^#](x1, x2, x3) = [1] x1 + [1] x3 + [0]
                                                           
    [merge#3^#](x1, x2, x3, x4, x5) = [1] x3 + [1] x5 + [1]
                                                           
                  [mergesort^#](x1) = [1] x1 + [1]
                                                  
                [mergesort#1^#](x1) = [1] x1 + [1]
                                                  
            [mergesort#2^#](x1, x2) = [1] x1 + [2]
                                                  
                [mergesort#3^#](x1) = [1] x1 + [1]
                                                  
                     [msplit^#](x1) = [0]
                                         
                   [msplit#1^#](x1) = [0]
                                         
               [msplit#2^#](x1, x2) = [0]
                                         
           [msplit#3^#](x1, x2, x3) = [0]
                                         
                          [c_1](x1) = [1] x1 + [0]
                                                  
                          [c_2](x1) = [1] x1 + [0]
                                                  
                          [c_3](x1) = [1] x1 + [0]
                                                  
                          [c_4](x1) = [1] x1 + [0]
                                                  
                          [c_5](x1) = [1] x1 + [0]
                                                  
                         [c_10](x1) = [0]
                                         
                         [c_11](x1) = [0]
                                         
                         [c_12](x1) = [0]
  
  This order satisfies following ordering constraints
  
                     [#compare(#0(), #0())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#EQ()]                                          
                                                                                                
                 [#compare(#0(), #neg(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#GT()]                                          
                                                                                                
                 [#compare(#0(), #pos(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#LT()]                                          
                                                                                                
                   [#compare(#0(), #s(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#LT()]                                          
                                                                                                
                 [#compare(#neg(@x), #0())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#LT()]                                          
                                                                                                
             [#compare(#neg(@x), #neg(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#compare(@y, @x)]                               
                                                                                                
             [#compare(#neg(@x), #pos(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#LT()]                                          
                                                                                                
                 [#compare(#pos(@x), #0())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#GT()]                                          
                                                                                                
             [#compare(#pos(@x), #neg(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#GT()]                                          
                                                                                                
             [#compare(#pos(@x), #pos(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#compare(@x, @y)]                               
                                                                                                
                   [#compare(#s(@x), #0())] =  [0]                                              
                                            >= [0]                                              
                                            =  [#GT()]                                          
                                                                                                
                 [#compare(#s(@x), #s(@y))] =  [0]                                              
                                            >= [0]                                              
                                            =  [#compare(@x, @y)]                               
                                                                                                
                          [merge(@l1, @l2)] =  [1] @l1 + [1] @l2 + [0]                          
                                            >= [1] @l1 + [1] @l2 + [0]                          
                                            =  [merge#1(@l1, @l2)]                              
                                                                                                
                [merge#1(::(@x, @xs), @l2)] =  [1] @l2 + [1] @xs + [1]                          
                                            >= [1] @l2 + [1] @xs + [1]                          
                                            =  [merge#2(@l2, @x, @xs)]                          
                                                                                                
                      [merge#1(nil(), @l2)] =  [1] @l2 + [0]                                    
                                            >= [1] @l2 + [0]                                    
                                            =  [@l2]                                            
                                                                                                
            [merge#2(::(@y, @ys), @x, @xs)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [merge#3(#less(@x, @y), @x, @xs, @y, @ys)]       
                                                                                                
                  [merge#2(nil(), @x, @xs)] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [::(@x, @xs)]                                    
                                                                                                
      [merge#3(#false(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [::(@y, merge(::(@x, @xs), @ys))]                
                                                                                                
       [merge#3(#true(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [2]                          
                                            >= [1] @xs + [1] @ys + [2]                          
                                            =  [::(@x, merge(@xs, ::(@y, @ys)))]                
                                                                                                
                            [mergesort(@l)] =  [1] @l + [0]                                     
                                            >= [1] @l + [0]                                     
                                            =  [mergesort#1(@l)]                                
                                                                                                
                [mergesort#1(::(@x1, @xs))] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [mergesort#2(@xs, @x1)]                          
                                                                                                
                       [mergesort#1(nil())] =  [0]                                              
                                            >= [0]                                              
                                            =  [nil()]                                          
                                                                                                
          [mergesort#2(::(@x2, @xs'), @x1)] =  [1] @xs' + [2]                                   
                                            >= [1] @xs' + [2]                                   
                                            =  [mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))]    
                                                                                                
                  [mergesort#2(nil(), @x1)] =  [1]                                              
                                            >= [1]                                              
                                            =  [::(@x1, nil())]                                 
                                                                                                
                               [msplit(@l)] =  [1] @l + [0]                                     
                                            >= [1] @l + [0]                                     
                                            =  [msplit#1(@l)]                                   
                                                                                                
           [mergesort#3(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [0]                          
                                            >= [1] @l1 + [1] @l2 + [0]                          
                                            =  [merge(mergesort(@l1), mergesort(@l2))]          
                                                                                                
                   [msplit#1(::(@x1, @xs))] =  [1] @xs + [1]                                    
                                            >= [1] @xs + [1]                                    
                                            =  [msplit#2(@xs, @x1)]                             
                                                                                                
                          [msplit#1(nil())] =  [0]                                              
                                            >= [0]                                              
                                            =  [tuple#2(nil(), nil())]                          
                                                                                                
             [msplit#2(::(@x2, @xs'), @x1)] =  [1] @xs' + [2]                                   
                                            >= [1] @xs' + [2]                                   
                                            =  [msplit#3(msplit(@xs'), @x1, @x2)]               
                                                                                                
                     [msplit#2(nil(), @x1)] =  [1]                                              
                                            >= [1]                                              
                                            =  [tuple#2(::(@x1, nil()), nil())]                 
                                                                                                
    [msplit#3(tuple#2(@l1, @l2), @x1, @x2)] =  [1] @l1 + [1] @l2 + [2]                          
                                            >= [1] @l1 + [1] @l2 + [2]                          
                                            =  [tuple#2(::(@x1, @l1), ::(@x2, @l2))]            
                                                                                                
                        [merge^#(@l1, @l2)] =  [1] @l1 + [1] @l2 + [0]                          
                                            >= [1] @l1 + [1] @l2 + [0]                          
                                            =  [c_1(merge#1^#(@l1, @l2))]                       
                                                                                                
              [merge#1^#(::(@x, @xs), @l2)] =  [1] @l2 + [1] @xs + [1]                          
                                            >  [1] @l2 + [1] @xs + [0]                          
                                            =  [c_2(merge#2^#(@l2, @x, @xs))]                   
                                                                                                
          [merge#2^#(::(@y, @ys), @x, @xs)] =  [1] @xs + [1] @ys + [1]                          
                                            >= [1] @xs + [1] @ys + [1]                          
                                            =  [c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))]
                                                                                                
    [merge#3^#(#false(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [1]                          
                                            >= [1] @xs + [1] @ys + [1]                          
                                            =  [c_4(merge^#(::(@x, @xs), @ys))]                 
                                                                                                
     [merge#3^#(#true(), @x, @xs, @y, @ys)] =  [1] @xs + [1] @ys + [1]                          
                                            >= [1] @xs + [1] @ys + [1]                          
                                            =  [c_5(merge^#(@xs, ::(@y, @ys)))]                 
                                                                                                
                          [mergesort^#(@l)] =  [1] @l + [1]                                     
                                            >= [1] @l + [1]                                     
                                            =  [mergesort#1^#(@l)]                              
                                                                                                
              [mergesort#1^#(::(@x1, @xs))] =  [1] @xs + [2]                                    
                                            >= [1] @xs + [2]                                    
                                            =  [mergesort#2^#(@xs, @x1)]                        
                                                                                                
        [mergesort#2^#(::(@x2, @xs'), @x1)] =  [1] @xs' + [3]                                   
                                            >= [1] @xs' + [3]                                   
                                            =  [mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))]  
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [1]                          
                                            >  [1] @l1 + [1] @l2 + [0]                          
                                            =  [merge^#(mergesort(@l1), mergesort(@l2))]        
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [1]                          
                                            >= [1] @l1 + [1]                                    
                                            =  [mergesort^#(@l1)]                               
                                                                                                
         [mergesort#3^#(tuple#2(@l1, @l2))] =  [1] @l1 + [1] @l2 + [1]                          
                                            >= [1] @l2 + [1]                                    
                                            =  [mergesort^#(@l2)]                               
                                                                                                

Consider the set of all dependency pairs

DPs:
  { 1: merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , 2: merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , 3: merge#2^#(::(@y, @ys), @x, @xs) ->
       c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , 4: merge#3^#(#false(), @x, @xs, @y, @ys) ->
       c_4(merge^#(::(@x, @xs), @ys))
  , 5: merge#3^#(#true(), @x, @xs, @y, @ys) ->
       c_5(merge^#(@xs, ::(@y, @ys)))
  , 6: mergesort^#(@l) -> mergesort#1^#(@l)
  , 7: mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , 8: mergesort#2^#(::(@x2, @xs'), @x1) ->
       mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , 9: mergesort#3^#(tuple#2(@l1, @l2)) ->
       merge^#(mergesort(@l1), mergesort(@l2))
  , 10: mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , 11: mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2,9}. These cover all (indirect) predecessors of dependency
pairs {1,2,3,4,5,9}, their number of application is equally
bounded. The dependency pairs are shifted into the corresponding
weak component(s).

We apply the transformation 'removetails' on the sub-problem:

Weak DPs:
  { merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
  , merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
  , merge#2^#(::(@y, @ys), @x, @xs) ->
    c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
  , merge#3^#(#false(), @x, @xs, @y, @ys) ->
    c_4(merge^#(::(@x, @xs), @ys))
  , merge#3^#(#true(), @x, @xs, @y, @ys) ->
    c_5(merge^#(@xs, ::(@y, @ys)))
  , mergesort^#(@l) -> mergesort#1^#(@l)
  , mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
  , mergesort#2^#(::(@x2, @xs'), @x1) ->
    mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#3^#(tuple#2(@l1, @l2)) ->
    merge^#(mergesort(@l1), mergesort(@l2))
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
  , mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
StartTerms: basic terms
Strategy: innermost

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ merge^#(@l1, @l2) -> c_1(merge#1^#(@l1, @l2))
, merge#1^#(::(@x, @xs), @l2) -> c_2(merge#2^#(@l2, @x, @xs))
, merge#2^#(::(@y, @ys), @x, @xs) ->
  c_3(merge#3^#(#less(@x, @y), @x, @xs, @y, @ys))
, merge#3^#(#false(), @x, @xs, @y, @ys) ->
  c_4(merge^#(::(@x, @xs), @ys))
, merge#3^#(#true(), @x, @xs, @y, @ys) ->
  c_5(merge^#(@xs, ::(@y, @ys)))
, mergesort^#(@l) -> mergesort#1^#(@l)
, mergesort#1^#(::(@x1, @xs)) -> mergesort#2^#(@xs, @x1)
, mergesort#2^#(::(@x2, @xs'), @x1) ->
  mergesort#3^#(msplit(::(@x1, ::(@x2, @xs'))))
, mergesort#3^#(tuple#2(@l1, @l2)) ->
  merge^#(mergesort(@l1), mergesort(@l2))
, mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l1)
, mergesort#3^#(tuple#2(@l1, @l2)) -> mergesort^#(@l2) }


We apply the transformation 'usablerules' on the sub-problem:

Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , merge#1(nil(), @l2) -> @l2
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , mergesort(@l) -> mergesort#1(@l)
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#1(nil()) -> nil()
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , msplit(@l) -> msplit#1(@l)
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2)) }
StartTerms: basic terms
Strategy: innermost

No rule is usable, rules are removed from the input problem.


We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Wall-time: 4.723952s
CPU-time: 21.177s

Wall-time: 7.643096s
CPU-time: 44.802s

Hurray, we answered YES(O(1),O(n^2))